Inference at * 
Iof proof for Lemma adjacent-sublist:


  T:Type, L1, L2:(T List). L1  L2  (x, y:T. adjacent(T;L1;x;y)  x before y  L2) 

latex

 by ((Auto) 
CollapseTHEN (((((FLemma `l_before_sublist` [4]) 
CollapseTHENA (Auto))) 

CoCollapseTHEN ((((((if ((-1) = 0) then BackThruSomeHyp else BHyp (-1) )) 
CollapseTHEN (Auto))
C) 
CollapseTHEN (((BLemma `adjacent-before`) 
CollapseTHEN (Auto)))))))) 

latex

C.

Definitions	{T}, L1  L2, type List, Type, P  Q, x before y  l, adjacent(T;L;x;y), x:A. B(x), x:AB(x)
Lemmas	sublist wf, adjacent wf, l before sublist, l before wf, adjacent-before